Failed to solve the following constraints:
  Is empty: n ≡ su (λ _ → n) (stuck)
      [ at Issue4995.agda:24,10-12 ]
